1. Technical Field
The present invention relates in general to data processing and, in particular, to software modeling.
2. Description of the Related Art
As software systems steadily grow in complexity and size, designing software systems manually becomes more and more error-prone. Recently, a new generation of lightweight software design tools has been developed that supports the formulation of software designs formally and the checking of the designs for correctness. The ALLOY™ tool-set, which was developed at Massachusetts Institute of Technology (MIT) by the Software Design Group, is one such design tool that is rapidly gaining prominence. With this tool-set, a system, such as a software system, is described in the ALLOY modeling language and then analyzed utilizing the ALLOY Analyzer. The ALLOY Analyzer 4.0, an accompanying tutorial, and related materials are freely available for download from the Alloy web site hosted by MIT (alloy dot mit dot edu).
ALLOY™ is a first-order relational modeling language with transitive closure and is particularly suited for expressing integrity properties of structurally complex data that arise in various contexts. ALLOY formulas describe infinite software designs and specifications and are undecidable. To make ALLOY formulas amenable to automated analysis, such as generation of instances of invariants, simulation of execution, and checking user-specified properties of a model, the ALLOY Analyzer finitizes the models using a scope as an upper bound on the cardinality of sets of typed objects. Analyses based on fnitization are inspired by the small scope hypothesis, which observes that many errors can be detected using small configurations, even in the case of large software systems. The ALLOY Analyzer encodes relations between objects as bit-matrices of atomic propositions with true and false values. The ALLOY Analyzer then formalizes the specification in question as a pure combinational Boolean predicate. The ALLOY Analyzer expresses the predicate in conjunctive normal form (CNF) and then decides its validity using an off-the-shelf satisfiability (SAT) solver.
SAT solvers often face an exponential expansion (often called “blow up”) in the number of possible assignments to the atomic propositions. This problem, known as state explosion, along with the large number of variables used in the CNF encoding, often limits the SAT-based ALLOY analysis to scopes below 10, rendering such analysis inapplicable to complex real-world designs.